YES 0.6970000000000001
H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:
↳ HASKELL
↳ LR
mainModule Main
| ((sequence :: [[a]] -> [[a]]) :: [[a]] -> [[a]]) |
module Main where
Lambda Reductions:
The following Lambda expression
\xs→return (x : xs)
is transformed to
sequence0 | x xs | = return (x : xs) |
The following Lambda expression
\x→sequence cs >>= sequence0 x
is transformed to
sequence1 | cs x | = sequence cs >>= sequence0 x |
↳ HASKELL
↳ LR
↳ HASKELL
↳ BR
mainModule Main
| ((sequence :: [[a]] -> [[a]]) :: [[a]] -> [[a]]) |
module Main where
Replaced joker patterns by fresh variables and removed binding patterns.
↳ HASKELL
↳ LR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
mainModule Main
| ((sequence :: [[a]] -> [[a]]) :: [[a]] -> [[a]]) |
module Main where
Cond Reductions:
The following Function with conditions
is transformed to
undefined0 | True | = undefined |
undefined1 | | = undefined0 False |
↳ HASKELL
↳ LR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
mainModule Main
| (sequence :: [[a]] -> [[a]]) |
module Main where
Haskell To QDPs
↳ HASKELL
↳ LR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_psPs(:(vx60, vx61), vx4, ba) → new_psPs(vx61, vx4, ba)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_psPs(:(vx60, vx61), vx4, ba) → new_psPs(vx61, vx4, ba)
The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3
↳ HASKELL
↳ LR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_gtGtEs(:(vx510, vx511), vx300, ba) → new_gtGtEs(vx511, vx300, ba)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_gtGtEs(:(vx510, vx511), vx300, ba) → new_gtGtEs(vx511, vx300, ba)
The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3
↳ HASKELL
↳ LR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
Q DP problem:
The TRS P consists of the following rules:
new_gtGtEs0(:(vx300, vx301), vx31, ba) → new_psPs0(vx31, vx300, new_gtGtEs1(vx301, vx31, ba), ba)
new_psPs0(vx31, vx300, vx4, ba) → new_sequence(vx31, ba)
new_sequence(:(:(vx300, vx301), vx31), ba) → new_gtGtEs0(vx301, vx31, ba)
new_gtGtEs0(:(vx300, vx301), vx31, ba) → new_gtGtEs0(vx301, vx31, ba)
new_sequence(:(:(vx300, vx301), vx31), ba) → new_psPs0(vx31, vx300, new_gtGtEs1(vx301, vx31, ba), ba)
The TRS R consists of the following rules:
new_gtGtEs1([], vx31, ba) → []
new_psPs3(vx31, vx300, vx4, ba) → new_psPs4(new_sequence0(vx31, ba), vx300, vx4, ba)
new_psPs5(vx4, ba) → vx4
new_gtGtEs2(:(vx510, vx511), vx300, ba) → new_psPs1(:(:(vx300, vx510), []), new_gtGtEs2(vx511, vx300, ba), ba)
new_gtGtEs1(:(vx300, vx301), vx31, ba) → new_psPs3(vx31, vx300, new_gtGtEs1(vx301, vx31, ba), ba)
new_sequence0([], ba) → :([], [])
new_psPs1([], vx4, ba) → vx4
new_psPs2(vx300, vx50, vx6, vx4, ba) → :(:(vx300, vx50), new_psPs1(vx6, vx4, ba))
new_psPs4(:(vx50, vx51), vx300, vx4, ba) → new_psPs2(vx300, vx50, new_psPs5(new_gtGtEs2(vx51, vx300, ba), ba), vx4, ba)
new_psPs4([], vx300, vx4, ba) → new_psPs5(vx4, ba)
new_gtGtEs2([], vx300, ba) → []
new_sequence0(:(vx30, vx31), ba) → new_gtGtEs1(vx30, vx31, ba)
new_psPs1(:(vx60, vx61), vx4, ba) → :(vx60, new_psPs1(vx61, vx4, ba))
The set Q consists of the following terms:
new_psPs4(:(x0, x1), x2, x3, x4)
new_sequence0(:(x0, x1), x2)
new_gtGtEs2(:(x0, x1), x2, x3)
new_sequence0([], x0)
new_psPs5(x0, x1)
new_gtGtEs1(:(x0, x1), x2, x3)
new_psPs1(:(x0, x1), x2, x3)
new_gtGtEs2([], x0, x1)
new_psPs1([], x0, x1)
new_psPs2(x0, x1, x2, x3, x4)
new_psPs4([], x0, x1, x2)
new_gtGtEs1([], x0, x1)
new_psPs3(x0, x1, x2, x3)
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_psPs0(vx31, vx300, vx4, ba) → new_sequence(vx31, ba)
The graph contains the following edges 1 >= 1, 4 >= 2
- new_sequence(:(:(vx300, vx301), vx31), ba) → new_gtGtEs0(vx301, vx31, ba)
The graph contains the following edges 1 > 1, 1 > 2, 2 >= 3
- new_gtGtEs0(:(vx300, vx301), vx31, ba) → new_gtGtEs0(vx301, vx31, ba)
The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3
- new_sequence(:(:(vx300, vx301), vx31), ba) → new_psPs0(vx31, vx300, new_gtGtEs1(vx301, vx31, ba), ba)
The graph contains the following edges 1 > 1, 1 > 2, 2 >= 4
- new_gtGtEs0(:(vx300, vx301), vx31, ba) → new_psPs0(vx31, vx300, new_gtGtEs1(vx301, vx31, ba), ba)
The graph contains the following edges 2 >= 1, 1 > 2, 3 >= 4